Example 1.2 in [Lucas - ENTCS64]

Summary: Ex1_2_Luc02c

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. Zantema's transformation (MuTerm)
  2. Ferreira and Ribeiro's transformation (MuTerm)
  3. Giesl and Middeldorp's transformation (MuTerm)
  4. Polynomial interpretation (MuTerm)
  5. CSDP
  6. CSRPO

CS-TRS Ex1_2_Luc02c (file Ex1_2_Luc02c.csr)

Functions:  2nd cons from s

Constructors:  cons s

Variables:  X Y Z

Arities: 

ar(2nd) = 1
ar(cons) = 2
ar(from) = 1
ar(s) = 1

Replacement map: 

µ(2nd)={1}
µ(cons)={1}
µ(from)={1}
µ(s)={1}

Rules:  (file Ex1_2_Luc02c)   

2nd(cons(X,cons(Y,Z))) -> Y
from(X) -> cons(X,from(s(X)))

The CS-TRS in OBJ format (file Ex1_2_Luc02c.obj):

obj Ex1_2_Luc02c is
  sort S .
  op 2nd : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op from : S -> S .
  op s : S -> S .
  vars X Y Z : S .
  eq 2nd(cons(X,cons(Y,Z))) = Y .
  eq from(X) = cons(X,from(s(X))) .
endo

Negative results

1. The µ-termination of Ex1_2_Luc02c cannot be proved by using Lucas' transformation. The TRS Ex1_2_Luc02c_L:

       2nd(cons(X)) -> Y
       from(X) -> cons(X)
       

   contains extra variables.

Positive results

1. The µ-termination of Ex1_2_Luc02c can be proved by using Zantema's transformation. The TRS Ex1_2_Luc02c_Z:

       2nd(cons(X,n__cons(Y,Z))) -> activate(Y)
       from(X) -> cons(X,n__from(s(X)))
       cons(X1,X2) -> n__cons(X1,X2)
       from(X) -> n__from(X)
       activate(n__cons(X1,X2)) -> cons(X1,X2)
       activate(n__from(X)) -> from(X)
       activate(X) -> X
       

   is terminating (use MuTerm).
2. The µ-termination of Ex1_2_Luc02c can be proved by using Ferreira and Ribeiro's transformation. The TRS Ex1_2_Luc02c_FR:

       2nd(cons(X,n__cons(Y,Z))) -> activate(Y)
       from(X) -> cons(X,n__from(n__s(X)))
       cons(X1,X2) -> n__cons(X1,X2)
       from(X) -> n__from(X)
       s(X) -> n__s(X)
       activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
       activate(n__from(X)) -> from(activate(X))
       activate(n__s(X)) -> s(activate(X))
       activate(X) -> X
       

   is terminating (use MuTerm).
3. The µ-termination of Ex1_2_Luc02c can be proved by using Giesl and Middeldorp's transformation. The TRS Ex1_2_Luc02c_GM:

       a__2nd(cons(X,cons(Y,Z))) -> mark(Y)
       a__from(X) -> cons(mark(X),from(s(X)))
       mark(2nd(X)) -> a__2nd(mark(X))
       mark(from(X)) -> a__from(mark(X))
       mark(cons(X1,X2)) -> cons(mark(X1),X2)
       mark(s(X)) -> s(mark(X))
       a__2nd(X) -> 2nd(X)
       a__from(X) -> from(X)
       

   is terminating (use MuTerm).
4. The µ-termination of Ex1_2_Luc02c can be proved by using the following polynomial interpretation (computed with MuTerm):

       [2nd](X) = X + 1
       [cons](X1,X2) = 2.X1 + 1/2.X2
       [from](X) = 4.X + 1
       [s](X) = X
       

5. The µ-termination of Ex1_2_Luc02c can be proved by using CSDP (computed by MuTerm).
6. The µ-termination of Ex1_2_Luc02c can also be proved by using CSRPO (computed by MuTerm).